\begin{tabbing}
$\forall$\=${\it es}$:event\_system\{i:l\}, $i$,$x$:Id, ${\it ds}$:fpf(Id; $x$.Type), $k$:Knd, $T$:Type,\+
\\[0ex]$f$:(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$rationals$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)).
\-\-\\[0ex]effect\_p(${\it es}$; $i$; ${\it ds}$; $k$; $T$; $x$; $f$) $\in$ prop\{i:l\}
\end{tabbing}